Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen. Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma linguística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais económica, a lógica.

Na notação formal utilizamos conectivos lógicos, operadores que realizam a ligação entre os átomos (os menores objetos). São eles:

• ${\displaystyle \neg }$ - Negação (não é um conectivo, simplesmente nega a fórmula ou átomo ligado)
• ${\displaystyle \land }$ - Conjunção
• ${\displaystyle \lor }$ - Disjunção
• ${\displaystyle \rightarrow }$ - Implicação
• ${\displaystyle \leftrightarrow }$ - Bi-implicação

No caso da lógica clássica de primeira ordem, temos ainda os quantificadores:

• ${\displaystyle \forall }$ - Universal
• ${\displaystyle \exists }$ - Existencial

Também utilizamos alguns símbolos extras para auxiliar:

• ${\displaystyle \vdash }$ - Derivação
• ${\displaystyle \vDash }$ - Consequência semântica
• ${\displaystyle \top }$ - Top (Verdade)
• ${\displaystyle \bot }$ - Bottom (Absurdo, falsidade)